\begin{tabbing}
msga{-}body\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$:Id fp$\rightarrow$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Void)\+
\\[0ex]$\times$$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;locl($a$))$\rightarrow$Prop$_{\mbox{\scriptsize i}}$
\\[0ex]$\times$${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kx}$))$\rightarrow$fpf{-}cap(${\it ds}$;IdDeq;2of(${\it kx}$);Void)
\\[0ex]$\times$\=${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$\+
\\[0ex](\=${\it tg}$:Id\+
\\[0ex]$\times$(\=State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kl}$))$\rightarrow$\+
\\[0ex](fpf{-}cap(${\it da}$;KindDeq;rcv(2of(${\it kl}$),${\it tg}$);Void) List))) List
\-\-\-\\[0ex]$\times$$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$${\it ltg}$:IdLnk$\times$Id fp$\rightarrow$ Knd List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ Id List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ IdLnk List
\\[0ex]$\times$${\it ltg}$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$Top
\-
\end{tabbing}